Practice Problems and Solutions 6 -- Beta Reduction of Lambda Expressions
You should do these problems on paper or mentally first, and only THEN check the solution.
For the follow problems, disambiguate by giving the fully-parenthesized term. Remember that
application is left-associative, and the lambda binding takes in as much right context as possible!
6.0. x y z w
Show Solution
6.1. x (y z) (w v x)
Show Solution
( ( x (y z) ) ( ( w v ) x ) )
6.2. λy. y x x
Show Solution
6.3. x λy. y x
Show Solution
( x ( λy. ( y x ) ) )
Yeah, this is a weird example, and you probably wouldn't write this, but
if you follow the rules, there is only one way to parenthesize it. Usually
best to start from the right.
6.4. λy. λy. f y x
Show Solution
( λy. ( λy. ( ( f y ) x ) ) )
6.5. f λy. ( x λy. y ) x
Show Solution
( f ( λy. ( ( x ( λy. y ) ) x ) ) )
6.6. f λy. x λy. y x
Show Solution
( f ( λy. ( x ( λy. ( y x ) ) ) ) )
Another weird one, but just follow the rules!
For the next set of problems, give the equivalent expression with the fewest parentheses.
6.7. ( ( ( x y ) z ) w )
Show Solution
6.8. ( ( x y ) ( z w ) )
Show Solution
6.9. ( λx. ( λy. ( ( y x ) w ) ) )
Show Solution
6.10. ( ( λy. ( y ( x w ) ) ) x )
Show Solution
6.11. ( ( (λx. x) (λy. y) ) ( (λz. z) w ) )
Show Solution
(λx. x) ( λy. y ) ( (λz. z) w )
or
( (λx. x) λy. y ) ( (λz. z) w )
For the following problems, underline all beta-redexes.
6.12. (λx. x) (λy. y) ( (λz. z) w )
Show Solution
(λx. x) (λy. y) ( (λz. z) w )
--------------- ---------
6.13. (λx. x) ( (λy. y) (λz. z) ) w
Show Solution
(λx. x) ( (λy. y) (λz. z) ) w
---------------------------
---------------
6.14. (λz. λx. x ( ( λx. z x ) y ) ) ( (λz. z) x )
Show Solution
(λz. λx. x ( ( λx. z x ) y ) ) ( (λz. z) x )
--------------------------------------------
------------- ---------
6.15. x y ( λx. z )
Show Solution
x y ( λx. z )
Trick question! There are no redexes!
In the following problems, you must reduce the terms to normal form; there is only one redex in each
step, so no choice about which redex to apply.
Except for the last few problems in this set of practice problems, where it is noted, in none of these do you have to worry
about free-variable capture and changing the bound variable using alpha-conversion.
6.16. Reduce: ( ( λx. x ) ( λy. y ) ) z
Show Solution
( ( λx. x ) ( λy. y ) ) z
=> ( λy. y ) z
=> z
6.17. Reduce: ( λx. x ) ( λy. y ) ( λz. z )
Show Solution
( ( λx. x ) ( λy. y ) ) ( λz. z )
=> ( λy. y ) ( λz. z )
=> ( λz. z )
6.18. Reduce: ( λx. x y ) ( λy. y x ) ( λz. z w )
Show Solution
( λx. x y ) ( λy. y x ) ( λz. z w )
=> ( ( λy. y x ) y ) ( λz. z w )
=> ( y x ) ( λz. z w )
For the following lambda expressions, reduce to normal form, using the order (normal or applicative) as indicated. Remember the rule: in normal order, the leftmost redex is reduced, and in applicative the right-most redex is reduced. So, scan through the expression and look for the leftmost (respectively, rightmost) lambda symbol in a redex. You will see that either of these ends up with the same normal form, due to the confluence property of beta-reduction.
6.19. Reduce using normal order: ( λx. ( λy. y x ) w ) z
Show Solution
( λx. ( λy. y x ) w ) z
=> ( λy. y z ) w
=> w z
6.20. Repeat 6.19 but using applicative order.
Show Solution
( λx. ( λy. y x ) w ) z
=> ( λx. w x) z
=> w z
6.21. Reduce using normal order: (λx. x) ((λy. y) ((λz. z) w))
Show Solution
(λx. x) ((λy. y) ((λz. z) w))
=> ((λy. y) ((λz. z) w))
=> (λz. z) w
=> w
6.22. Repeat 6.21 but using applicative order.
Show Solution
(λx. x) ((λy. y) ((λz. z) w))
=> (λx. x) ((λy. y) w )
=> (λx. x) w
=> w
6.23. Reduce using normal order: ( λx. x y ) ( λy. y x ) x
Show Solution
( λx. x y ) ( λy. y x ) x
=> ( ( λy. y x ) y ) x
=> y x x
6.24. Repeat 6.23 but using applicative order.
Show Solution
Trick question! The answer is the same, since there is only one redex in each term,
as you can see by adding parentheses:
( ( ( λx. x y ) ( λy. y x ) ) x )
=> ( ( ( λy. y x ) y ) x )
=> ( ( y x ) x )
6.25. Reduce using normal order: ( ( ( λx. x x ) ( λy. x y ) ) w )
Show Solution
( ( ( λx. x x ) ( λy. x y ) ) w )
=> ( ( ( λy. x y ) ( λy. x y ) ) w )
=> ( ( x ( λy. x y ) ) w )
6.26. Reduce using normal order: ( ( ( λx. ( x x ) ) ( λy. ( y x ) ) ) w )
Show Solution
( ( ( λx. ( x x ) ) ( λy. ( y x ) ) ) w )
=> ( ( ( λy. ( y x ) ) ( λy. ( y x ) ) ) w )
=> ( ( ( λy. ( y x ) ) x ) w )
=> ( ( x x ) w )
6.27. Reduce using normal order: ( ( ( λx. ( x w ) ) ( λy. ( v y ) ) ) ( w z ) )
Show Solution
( ( ( λx. ( x w ) ) ( λy. ( v y ) ) ) ( w z ) )
=> ( ( ( λy. ( v y ) ) w ) ( w z ) )
=> ( ( v w ) ( w z ) )
6.28. Reduce using normal order: ( ( λx. ( x ( x w ) ) ) ( ( λy. ( y v ) ) w ) )
Show Solution
( ( λx. ( x ( x w ) ) ) ( ( λy. ( y v ) ) w ) )
=> ( ( ( λy. ( y v ) ) w ) ( ( ( λy. ( y v ) ) w ) w ) )
=> ( ( w v ) ( ( ( λy. ( y v ) ) w ) w ) )
=> ( ( w v ) ( ( w v ) w ) )
6.29. Reduce using normal order: ( λx. ( λy. ( λz. x y ) x ) ) ( λw. w x ) ( λv. y v )
Show Solution
( λx. ( λy. ( λz. x y ) x ) ) ( λw. w x ) ( λv. y v )
=> ( λy. ( λz. ( λw. w x ) y ) ( λw. w x ) ) ( λv. y v )
=> ( λz. ( λw. w x ) ( λv. y v ) ) ( λw. w x )
=> ( λw. w x ) ( λv. y v )
=> ( λv. y v ) x
=> y x
6.30. Reduce using normal order: ( λx. ( λx. ( λy. x y ) ) ( λz. y z x ) ) w
Show Solution
( λx. ( λx. ( λy. x y ) ) ( λz. y z x ) ) w
=> ( λx. ( λy. x y ) ) ( λz. y z w )
=> ( λy. ( λz. y z w ) y )
=> ( λy. y y w )
6.31. Reduce using normal order: ( ( λf. ( λx. ( f ( f ( f x ) ) ) ) ) ( λz. ( w z ) ) )
Show Solution
( ( λf. ( λx. ( f ( f ( f x ) ) ) ) ) ( λz. ( w z ) ) )
=> ( λx. ( ( λz. ( w z ) ) ( ( λz. ( w z ) ) ( ( λz. ( w z ) ) x ) ) ) )
=> ( λx. ( w ( ( λz. ( w z ) ) ( ( λz. ( w z ) ) x ) ) ) )
=> ( λx. ( w ( w ( ( λz. ( w z ) ) x ) ) ) )
=> ( λx. ( w ( w ( w x ) ) ) )
6.32. Reduce using normal order: ( ( λf. ( λx. ( f ( f x ) ) ) ) ( λz. ( z w ) ) )
Show Solution
( ( λf. ( λx. ( f ( f x ) ) ) ) ( λz. ( z w ) ) )
=> ( λx. ( ( λz. ( z w ) ) ( ( λz. ( z w ) ) x ) ) )
=> ( λx. ( ( ( λz. ( z w ) ) x ) w ) )
=> ( λx. ( ( x w ) w ) )
6.33. Reduce using normal order: ( λf. f ( λx. ( λy. y) ) ( λx. (λy.x) ) ) ( λx. (λy. x) ) (This is lam_not (true) from Lab 04.)
Show Solution
(λf.f(λx.(λy.y))(λx.(λy.x)))(λx.(λy.x))
=> (λx.(λy.x))(λx.(λy.y))(λx.(λy.x))
=> (λy.(λx.(λy.y)))(λx.(λy.x))
=> (λx.(λy.y))
For the following two problems, "reduce" the expression until you see the pattern, and also explain the pattern in words.
6.34. (λx.x x) (λx.x x)
Show Solution
(λx.x x)(λx.x x)
=> (λx.x x)(λx.x x)
=> (λx.x x)(λx.x x) etc.
Repeats the exact same thing forever!
6.35. (λx.x x x) (λx.x x x)
Show Solution
(λx.x x x)(λx.x x x)
=> (λx.x x x)(λx.x x x)(λx.x x x)
=> (λx.x x x)(λx.x x x)(λx.x x x)(λx.x x x)
Keeps expanding by adding the same term to the end each time, forever!
6.36. ( λf. ( λx. f ( x x ) ) ( λx. f ( x x ) ) ) ( $ ) (This is called the "Y-Combinator." Assume $ is a constant -- Google "Y-Combinator" if you want to understand the joke!)
Show Solution
(λf.(λx.f(x x ))(λx.f(x x )))($)
=> (λx.$(x x ))(λx.$(x x ))
=> $((λx.$(x x ))(λx.$(x x )))
=> $($((λx.$(x x ))(λx.$(x x ))))
=> $($($((λx.$(x x ))(λx.$(x x )))))
=> $($($($((λx.$(x x ))(λx.$(x x ))))))
=> $($($($($((λx.$(x x ))(λx.$(x x )))))))
This keeps adding $ to the front of the term!
For the following problem, the reduction sequence involves "free variable capture"; perform the reduction as we did above, and then explain precisely what happens to change a free variable into a bound variable.
6.37. ( λf. ( λx. f(f x ) ) ) ( λz. z x )
Show Solution
The free variable in the argument is x (in red), the
binding occurrence of x in the function is in blue, and the bound
occurrence of x in the function is in green, with all the parts
of the expression labelled:
( λf. ( λx. f(f(x)) ) ) ( λz. z(x) )
--------------
body
----------------------- ------------
function argument
Replacing the occurrence of f in the body by the argument:
=> ( λx. f(f(x)) ) subst: [ (f, ( λz. z(x) ) ) ]
== ( λx. ( λz. z(x)) (( λz. z(x)) (x)) )
Now, free variable capture has occurred! The free variable x has become a bound occurrence inside the binding occurrence of x. This changes
the meaning of x (which may have been defined originally in an outer context).
=> ( λx. ( λz. z x ) x x )
=> ( λx. x x x )
For the following, reduce to normal form using normal-order reduction; avoid free variable capture by renaming: add a prime to any
bound variable which needs to be renamed to avoid capturing a free variable.
6.38. ( λx. ( λy. y x ) x ) y
Show Solution
( λx. ( λy. y x ) x ) y
=> ( λy'. y' y ) y
=> y y
6.39. ( λx. ( λy. y x ) x ) ( λx. x y )
Show Solution
( λx. ( λy. y x ) x ) ( λx. x y )
=> ( λy'. y' ( λx. x y ) ) ( λx. x y )
=> ( λx. x y ) ( λx. x y )
=> ( λx. x y ) y
=> y y
6.40. (λx.(λy.y(λy.y(λy.y x)))) y
Show Solution
(λx.(λy.y(λy.y(λy.y x)))) y
=> (λy'.y'(λy''.y''(λy'''.y''' y)))
or, technically, one could choose the same variable, since there would be no conflicts:
=> (λy'.y'(λy'.y'(λy'.y' y)))